es:ES, i, x:Id, P:(vartype(i;x)Prop). @i always.P(v)  Prop 

latex

Definitions	@i always.P(x), e@i. P(e), x. t(x), x(s), E, loc(e), Prop, Id, ES, x when e, t  T, vartype(i;x), x:A. B(x)
Lemmas	es-vartype wf, es-when wf, event system wf, Id wf, es-loc wf, es-E wf, alle-at wf